$\forall$$A$:MsgA, $x$, $z$:Id, $k$:Knd, $s_{1}$, $s_{2}$:$A$.(timed)state, $v$:$A$.da($k$).
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ ($\neg$$A$.rframe($k$ reads $x$))
\\[0ex]$\Rightarrow$ ma{-}x{-}tequiv($A$;$x$;$s_{1}$;$s_{2}$)
\\[0ex]$\Rightarrow$ ($\neg$($z$ = $x$))
\\[0ex]$\Rightarrow$ ($A$.ef($k$,$z$,read{-}state($s_{1}$),$v$)?$s_{1}$($z$) = $A$.ef($k$,$z$,read{-}state($s_{2}$),$v$)?$s_{2}$($z$) $\in$ $\mathbb{Q}\rightarrow$$A$.ds($z$))